<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>IndPrinciples: 归纳法则</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">IndPrinciples<span class="subtitle">归纳法则</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 在理解了柯里-霍华德同构及其 Coq 实现之后，我们就可以深入学习归纳法则了。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">ProofObjects</span>.<br/>
</div>

<div class="doc">
<a name="lab281"></a><h1 class="section">基础</h1>

<div class="paragraph"> </div>

 每当我们使用 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 来声明数据类型时，Coq 就会自动为该类型生成
    <b>归纳法则</b>。这个归纳法则也是定理：如果 <span class="inlinecode"><span class="id" type="var">t</span></span> 是归纳定义的，那么对应的
    归纳法则被称作 <span class="inlinecode"><span class="id" type="var">t_ind</span></span>。这是自然数的归纳法则： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">nat_ind</span>.<br/>
<span class="comment">(*&nbsp;&nbsp;===&gt;&nbsp;nat_ind&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall&nbsp;P&nbsp;:&nbsp;nat&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;Prop,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P&nbsp;0&nbsp;&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(forall&nbsp;n&nbsp;:&nbsp;nat,&nbsp;P&nbsp;n&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;P&nbsp;(S&nbsp;n))&nbsp;&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall&nbsp;n&nbsp;:&nbsp;nat,&nbsp;P&nbsp;n&nbsp;&nbsp;*)</span><br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="tactic">induction</span></span> 利用归纳法则，执行 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">t_ind</span></span> 等策略。
    为了清楚地理解这一点，让我们直接使用 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">nat_ind</span></span> 而非 <span class="inlinecode"><span class="id" type="tactic">induction</span></span>
    策略来证明。<a href="Basics.html"><span class="inlineref">Basics</span></a> 一章中 <span class="inlinecode"><span class="id" type="var">mult_0_r'</span></span> 定理的另一种证明如下所示。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">mult_0_r'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>:<span class="id" type="var">nat</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> * 0 = 0.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">nat_ind</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">n'</span> <span class="id" type="var">IHn'</span>. <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">IHn'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
这个证明基本上等同于之前的，但有几点区别值得注意。

<div class="paragraph"> </div>

    首先，在证明的归纳步骤（<span class="inlinecode">"<span class="id" type="var">S</span>"</span> 情形）中，我们不得不手动管理变量名（即 <span class="inlinecode"><span class="id" type="tactic">intros</span></span>），
    而 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 会自动完成这些。

<div class="paragraph"> </div>

    其次，在应用 <span class="inlinecode"><span class="id" type="var">nat_ind</span></span> 之前我们没有在上下文中引入 <span class="inlinecode"><span class="id" type="var">n</span></span> —— <span class="inlinecode"><span class="id" type="var">nat_ind</span></span> 的结论
    是一个带有量词的公式，<span class="inlinecode"><span class="id" type="tactic">apply</span></span> 需要这个结论精确地匹配当前证明目标状态的形状，包括其中的量词。
    相反，<span class="inlinecode"><span class="id" type="tactic">induction</span></span> 策略对于上下文中的变量或目标中由量词引入的变量都适用。

<div class="paragraph"> </div>

    相比于直接使用 <span class="inlinecode"><span class="id" type="var">nat_ind</span></span> 这样的归纳法则，在实践中使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 更加方便。
    但重要的是认识到除了这一点变量名的管理工作，我们在做的其实就是应用 <span class="inlinecode"><span class="id" type="var">nat_ind</span></span>。 
<div class="paragraph"> </div>

<a name="lab282"></a><h4 class="section">练习：2 星, standard, optional (plus_one_r')</h4>
 请不使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 策略来完成这个证明。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">plus_one_r'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>:<span class="id" type="var">nat</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> + 1 = <span class="id" type="var">S</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Coq 为每一个 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 定义的数据类型生成了归纳法则，包括那些非递归的。
    尽管我们不需要归纳，便可证明非递归数据类型的性质，但归纳原理仍可用来证明其性质；
    给定类型，及关于该类型所有值的性质，归纳原理提供了证明该性质的方法。

<div class="paragraph"> </div>

    这些生成的原则都具有类似的模式。如果我们定义了类型 <span class="inlinecode"><span class="id" type="var">t</span></span> 及其构造子 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> ... <span class="inlinecode"><span class="id" type="var">cn</span></span>，
    Coq 会生成形如下文的定理：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">t_ind</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span>&nbsp;:&nbsp;<span class="id" type="var">t</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;... <span class="id" type="tactic">case</span>&nbsp;<span class="id" type="keyword">for</span>&nbsp;<span class="id" type="var">c<sub>1</sub></span>&nbsp;... →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;... <span class="id" type="tactic">case</span>&nbsp;<span class="id" type="keyword">for</span>&nbsp;<span class="id" type="var">c<sub>2</sub></span>&nbsp;... →&nbsp;...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;... <span class="id" type="tactic">case</span>&nbsp;<span class="id" type="keyword">for</span>&nbsp;<span class="id" type="var">cn</span>&nbsp;... →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">t</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">n</span>
<div class="paragraph"> </div>

</div>
    每个情形具体的形状取决于对应构造子的参数。在尝试总结出一般规律前，
    让我们先来看看更多的例子。首先是一个无参数构造子的例子： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">yesno</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">yes</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">no</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">yesno_ind</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;yesno_ind&nbsp;:&nbsp;forall&nbsp;P&nbsp;:&nbsp;yesno&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;Prop,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P&nbsp;yes&nbsp;&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P&nbsp;no&nbsp;&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall&nbsp;y&nbsp;:&nbsp;yesno,&nbsp;P&nbsp;y&nbsp;*)</span><br/>
</div>

<div class="doc">
<a name="lab283"></a><h4 class="section">练习：1 星, standard, optional (rgb)</h4>
 对如下数据类型，请写出 Coq 将会生成的归纳法则。
    先在纸上或注释内写下你的答案，然后同 Coq 打印出的结果比较。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">rgb</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="tactic">red</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">green</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">blue</span>.<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">rgb_ind</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 下文例子中，有一个构造子调取多个参数。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">natlist</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">nnil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ncons</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">natlist</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">natlist_ind</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;(除了一些变量被重命名了)<br/>
&nbsp;&nbsp;&nbsp;natlist_ind&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall&nbsp;P&nbsp;:&nbsp;natlist&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;Prop,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P&nbsp;nnil&nbsp;&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(forall&nbsp;(n&nbsp;:&nbsp;nat)&nbsp;(l&nbsp;:&nbsp;natlist),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P&nbsp;l&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;P&nbsp;(ncons&nbsp;n&nbsp;l))&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall&nbsp;n&nbsp;:&nbsp;natlist,&nbsp;P&nbsp;n&nbsp;*)</span><br/>
</div>

<div class="doc">
<a name="lab284"></a><h4 class="section">练习：1 星, standard, optional (natlist1)</h4>
 假设我们写下的定义和上面的有一些区别： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">natlist1</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">nnil1</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">nsnoc1</span> (<span class="id" type="var">l</span> : <span class="id" type="var">natlist1</span>) (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>).<br/>
</div>

<div class="doc">
现在归纳法则会是什么呢？  <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

 对于这些例子，我们可以总结出一般的规则：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 类型定义给定了若干构造子；每个对应于归纳法则中的一个语句。

</li>
<li> 每个构造子 <span class="inlinecode"><span class="id" type="var">c</span></span> 有参数类型 <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> ... <span class="inlinecode"><span class="id" type="var">an</span></span>。

</li>
<li> 每个 <span class="inlinecode"><span class="id" type="var">ai</span></span> 要么是 <span class="inlinecode"><span class="id" type="var">t</span></span>（我们定义的数据类型），要么是其他的类型 <span class="inlinecode"><span class="id" type="var">s</span></span>。

</li>
<li> 对应的归纳法则情形则是：

<div class="paragraph"> </div>

<ul class="doclist">
<li> “对于所有的类型为 <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span>...<span class="inlinecode"><span class="id" type="var">an</span></span> 的值 <span class="inlinecode"><span class="id" type="var">x<sub>1</sub></span></span>...<span class="inlinecode"><span class="id" type="var">xn</span></span>，如果 <span class="inlinecode"><span class="id" type="var">P</span></span> 对每个
          归纳的参数（每个具有类型 <span class="inlinecode"><span class="id" type="var">t</span></span> 的 <span class="inlinecode"><span class="id" type="var">xi</span></span>）都成立，那么 <span class="inlinecode"><span class="id" type="var">P</span></span> 对于 <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">x<sub>1</sub></span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" type="var">xn</span></span>
          成立”。

</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>

<a name="lab285"></a><h4 class="section">练习：1 星, standard, optional (byntree_ind)</h4>
 对如下数据类型，请写出 Coq 将会生成的归纳法则。
   （与之前一样，先在纸上或注释内写下你的答案，然后同 Coq 打印出的结果比较。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">byntree</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;| <span class="id" type="var">bempty</span><br/>
&nbsp;| <span class="id" type="var">bleaf</span> (<span class="id" type="var">yn</span> : <span class="id" type="var">yesno</span>)<br/>
&nbsp;| <span class="id" type="var">nbranch</span> (<span class="id" type="var">yn</span> : <span class="id" type="var">yesno</span>) (<span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> : <span class="id" type="var">byntree</span>).<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab286"></a><h4 class="section">练习：1 星, standard, optional (ex_set)</h4>
 这是对一个归纳定义的集合的归纳法则。

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ExSet_ind</span>&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span>&nbsp;:&nbsp;<span class="id" type="var">ExSet</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span>&nbsp;:&nbsp;<span class="id" type="var">bool</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">con1</span>&nbsp;<span class="id" type="var">b</span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>)&nbsp;(<span class="id" type="var">e</span>&nbsp;:&nbsp;<span class="id" type="var">ExSet</span>),&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">e</span>&nbsp;→&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">con2</span>&nbsp;<span class="id" type="var">n</span>&nbsp;<span class="id" type="var">e</span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">e</span>&nbsp;:&nbsp;<span class="id" type="var">ExSet</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">e</span>
<div class="paragraph"> </div>

</div>
    请写出使用 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 来定义的 <span class="inlinecode"><span class="id" type="var">ExSet</span></span>： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ExSet</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab287"></a><h1 class="section">多态</h1>

<div class="paragraph"> </div>

 接下来，多态数据结构会是怎样呢？

<div class="paragraph"> </div>

    归纳定义的多态列表

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Inductive</span>&nbsp;<span class="id" type="var">list</span>&nbsp;(<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>)&nbsp;:&nbsp;<span class="id" type="keyword">Type</span>&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">nil</span>&nbsp;:&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">cons</span>&nbsp;:&nbsp;<span class="id" type="var">X</span>&nbsp;→&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>&nbsp;→&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>.
<div class="paragraph"> </div>

</div>
    同 <span class="inlinecode"><span class="id" type="var">natlist</span></span> 是十分相似的。主要的区别是，这里全部的定义是由集合 <span class="inlinecode"><span class="id" type="var">X</span></span> 所<b>参数化</b>的：
    也即，我们定义了<b>一族</b>归纳类型 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>，对于每个 <span class="inlinecode"><span class="id" type="var">X</span></span> 有其对应的类型在此族中。
    （请注意，当 <span class="inlinecode"><span class="id" type="var">list</span></span> 出现在声明体中时，它总是被应用参数 <span class="inlinecode"><span class="id" type="var">X</span></span>。）
    归纳法则同样被 <span class="inlinecode"><span class="id" type="var">X</span></span> 所参数化：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">list_ind</span>&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>&nbsp;:&nbsp;<span class="id" type="keyword">Type</span>)&nbsp;(<span class="id" type="var">P</span>&nbsp;:&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">P</span>&nbsp;[]&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">x</span>&nbsp;:&nbsp;<span class="id" type="var">X</span>)&nbsp;(<span class="id" type="var">l</span>&nbsp;:&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>),&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">x</span>&nbsp;::&nbsp;<span class="id" type="var">l</span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>&nbsp;:&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">l</span>
<div class="paragraph"> </div>

</div>
    请注意归纳法则的<b>所有部分</b>都被 <span class="inlinecode"><span class="id" type="var">X</span></span> 所参数化。也即，<span class="inlinecode"><span class="id" type="var">list_ind</span></span> 可认为是一个
    多态函数，当被应用类型 <span class="inlinecode"><span class="id" type="var">X</span></span> 时，返回特化在类型 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 上的归纳法则。 
<div class="paragraph"> </div>

<a name="lab288"></a><h4 class="section">练习：1 星, standard, optional (tree)</h4>
 对如下数据类型，请写出 Coq 将会生成的归纳法则，并与 Coq 打印出的结果比较。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">tree</span> (<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">leaf</span> (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">node</span> (<span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub></span> : <span class="id" type="var">tree</span> <span class="id" type="var">X</span>).<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">tree_ind</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab289"></a><h4 class="section">练习：1 星, standard, optional (mytype)</h4>
 请找到对应于以下归纳法则的归纳定义：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">mytype_ind</span>&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>&nbsp;:&nbsp;<span class="id" type="keyword">Type</span>)&nbsp;(<span class="id" type="var">P</span>&nbsp;:&nbsp;<span class="id" type="var">mytype</span>&nbsp;<span class="id" type="var">X</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>&nbsp;:&nbsp;<span class="id" type="var">X</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">constr1</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">x</span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">constr2</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">n</span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span>&nbsp;:&nbsp;<span class="id" type="var">mytype</span>&nbsp;<span class="id" type="var">X</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">m</span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">constr3</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">m</span>&nbsp;<span class="id" type="var">n</span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span>&nbsp;:&nbsp;<span class="id" type="var">mytype</span>&nbsp;<span class="id" type="var">X</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">m</span>
<div class="paragraph"> </div>

</div>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab290"></a><h4 class="section">练习：1 星, standard, optional (foo)</h4>
 请找到对应于以下归纳法则的归纳定义：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">foo_ind</span>&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;:&nbsp;<span class="id" type="keyword">Type</span>)&nbsp;(<span class="id" type="var">P</span>&nbsp;:&nbsp;<span class="id" type="var">foo</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>&nbsp;:&nbsp;<span class="id" type="var">X</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">bar</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;<span class="id" type="var">x</span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">y</span>&nbsp;:&nbsp;<span class="id" type="var">Y</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">baz</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;<span class="id" type="var">y</span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">f<sub>1</sub></span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="var">foo</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">Y</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">f<sub>1</sub></span>&nbsp;<span class="id" type="var">n</span>))&nbsp;→&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">quux</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;<span class="id" type="var">f<sub>1</sub></span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">f<sub>2</sub></span>&nbsp;:&nbsp;<span class="id" type="var">foo</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">Y</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">f<sub>2</sub></span>
<div class="paragraph"> </div>

</div>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab291"></a><h4 class="section">练习：1 星, standard, optional (foo')</h4>
 请考虑以下归纳定义： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">foo'</span> (<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">C<sub>1</sub></span> (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) (<span class="id" type="var">f</span> : <span class="id" type="var">foo'</span> <span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">C<sub>2</sub></span>.<br/>
</div>

<div class="doc">
Coq 会为 <span class="inlinecode"><span class="id" type="var">foo'</span></span> 生成什么归纳法则？请填写下面的空白，并使用 Coq 检查你的答案。

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">foo'_ind</span>&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>&nbsp;:&nbsp;<span class="id" type="keyword">Type</span>)&nbsp;(<span class="id" type="var">P</span>&nbsp;:&nbsp;<span class="id" type="var">foo'</span>&nbsp;<span class="id" type="var">X</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">l</span>&nbsp;:&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>)&nbsp;(<span class="id" type="var">f</span>&nbsp;:&nbsp;<span class="id" type="var">foo'</span>&nbsp;<span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">_______________________</span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">_______________________</span>&nbsp;&nbsp;&nbsp;)&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">___________________________________________</span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">f</span>&nbsp;:&nbsp;<span class="id" type="var">foo'</span>&nbsp;<span class="id" type="var">X</span>,&nbsp;<span class="id" type="var">________________________</span>
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>

 <span class="proofbox">&#9744;</span> 
</div>

<div class="doc">
<a name="lab292"></a><h1 class="section">归纳假设</h1>

<div class="paragraph"> </div>

 “归纳假设”是在什么语境下出现的呢？

<div class="paragraph"> </div>

    对于数的归纳法则：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">P</span>&nbsp;0&nbsp;&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">n</span>&nbsp;→&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;<span class="id" type="var">n</span>))&nbsp;&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>,&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">n</span>
<div class="paragraph"> </div>

</div>
  是一个对于所有命题 <span class="inlinecode"><span class="id" type="var">P</span></span> （或更严格地说，对由数字 <span class="inlinecode"><span class="id" type="var">n</span></span> 索引的所有命题 <span class="inlinecode"><span class="id" type="var">P</span></span>）
  都成立的泛化陈述。每次使用这个原理，我们将 <span class="inlinecode"><span class="id" type="var">P</span></span> 特化为一个类型为 <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>
  的表达式。

<div class="paragraph"> </div>

  通过命名这个表达式，我们可以让归纳证明更加明确。比如，除了陈述定理
  <span class="inlinecode"><span class="id" type="var">mult_0_r</span></span> 为 “<span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span>,</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">*</span> <span class="inlinecode">0</span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>”，我们还可以写成
  “<span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span>,</span> <span class="inlinecode"><span class="id" type="var">P_m0r</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>”，其中 <span class="inlinecode"><span class="id" type="var">O_m0r</span></span> 定义为…… 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">P_m0r</span> (<span class="id" type="var">n</span>:<span class="id" type="var">nat</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> * 0 = 0.<br/>
</div>

<div class="doc">
……或等价地： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">P_m0r'</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">fun</span> <span class="id" type="var">n</span> ⇒ <span class="id" type="var">n</span> * 0 = 0.<br/>
</div>

<div class="doc">
现在看看 <span class="inlinecode"><span class="id" type="var">P_m0r</span></span> 在证明中出现在哪里。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">mult_0_r''</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>:<span class="id" type="var">nat</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">P_m0r</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">nat_ind</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;请注意目前的证明状态！&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">IHn</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">P_m0r</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHn</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">P_m0r</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHn</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
通常我们并不会在证明中额外地为命题命名，但有意地进行一两个练习
    可以帮助我们清晰地看到哪个是归纳假设。
    如果对 <span class="inlinecode"><span class="id" type="var">n</span></span> 归纳来证明 <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span>,</span> <span class="inlinecode"><span class="id" type="var">P_m0r</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>（使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span>
    或 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">nat_ind</span></span>），可以看到第一个子目标要求我们证明 <span class="inlinecode"><span class="id" type="var">P_m0r</span></span> <span class="inlinecode">0</span>
    （“<span class="inlinecode"><span class="id" type="var">P</span></span> 对零成立”），而第二个子目标要求我们证明 <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>,</span> <span class="inlinecode"><span class="id" type="var">P_m0r</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P_m0r</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span>
    （也即，“<span class="inlinecode"><span class="id" type="var">P</span></span> 对 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> 成立仅当其对 <span class="inlinecode"><span class="id" type="var">n'</span></span> 成立”，或者说，“<span class="inlinecode"><span class="id" type="var">P</span></span> 被 <span class="inlinecode"><span class="id" type="var">S</span></span> 保持”）。
    <b>归纳假设</b>是后一个蕴含式中的前提部分，即假设 <span class="inlinecode"><span class="id" type="var">P</span></span> 对 <span class="inlinecode"><span class="id" type="var">n'</span></span> 成立，这是我们在证明 <span class="inlinecode"><span class="id" type="var">P</span></span>
    对 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> 的过程中允许使用的。 
</div>

<div class="doc">
<a name="lab293"></a><h1 class="section">深入 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 策略</h1>

<div class="paragraph"> </div>

 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 策略事实上为我们做了更多低层次的工作。

<div class="paragraph"> </div>

    请回忆一下自然数归纳法则的非形式化陈述：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 如果 <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 是某个涉及到数字 n 的命题，我们想要证明 <span class="inlinecode"><span class="id" type="var">P</span></span> 对于<b>所有</b>数字 n
        都成立，我们以如下方式推理：
<ul class="doclist">
<li> 证明 <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">0</span> 成立

</li>
<li> 证明如果 <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> 成立，那么 <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span> 成立

</li>
<li> 得出结论 <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 对所有 n 成立。

</li>
</ul>

</li>
</ul>
    因此，当以 <span class="inlinecode"><span class="id" type="tactic">intros</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 和 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 开始一个证明时，我们首先在告诉 Coq
    考虑一个<b>特殊的</b> <span class="inlinecode"><span class="id" type="var">n</span></span>（通过引入到上下文中），然后告诉它证明一些关于
    <b>全体</b>数字的性质（通过使用归纳）。

<div class="paragraph"> </div>

    在这种情况下，Coq 事实上在内部“二次一般化（re-generalize）”了我们归纳的变量。
    比如说，起初证明 <span class="inlinecode"><span class="id" type="var">plus</span></span> 的结合性时……  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">plus_assoc'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">p</span> : <span class="id" type="var">nat</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> + (<span class="id" type="var">m</span> + <span class="id" type="var">p</span>) = (<span class="id" type="var">n</span> + <span class="id" type="var">m</span>) + <span class="id" type="var">p</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;……首先，我们引入全部&nbsp;3&nbsp;个变量到上下文中，或者说是<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;“考虑任意的&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span>，<span class="inlinecode"><span class="id" type="var">m</span></span>&nbsp;和&nbsp;<span class="inlinecode"><span class="id" type="var">p</span></span>……”&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">p</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;……现在，我们用&nbsp;<span class="inlinecode"><span class="id" type="tactic">induction</span></span>&nbsp;策略来证明&nbsp;<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;（也即，<span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">+</span> <span class="inlinecode">(<span class="id" type="var">m</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">p</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" type="var">n</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">m</span>)</span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">p</span></span>）对全体的&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span>&nbsp;成立，<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;也因此对于当前上下文中特殊的&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span>&nbsp;也成立。&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;在&nbsp;<span class="inlinecode"><span class="id" type="tactic">induction</span></span>&nbsp;生成的第二个子目标——“归纳步骤”——我们必须证明<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;对全体&nbsp;<span class="inlinecode"><span class="id" type="var">n'</span></span>，<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>&nbsp;蕴含了&nbsp;<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span>。<span class="inlinecode"><span class="id" type="tactic">induction</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;策略自动为我们引入了&nbsp;<span class="inlinecode"><span class="id" type="var">n'</span></span>&nbsp;和&nbsp;<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>&nbsp;到上下文中，并保持&nbsp;<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;为目标。&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">IHn'</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
对目标中含有量词的变量应用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 同样可以工作。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">plus_comm'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> + <span class="id" type="var">m</span> = <span class="id" type="var">m</span> + <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">intros</span> <span class="id" type="var">m</span>. <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">plus_n_O</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" type="tactic">intros</span> <span class="id" type="var">m</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">IHn'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">plus_n_Sm</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
请注意，使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 后 <span class="inlinecode"><span class="id" type="var">m</span></span> 在目标中仍然是绑定的，
    也即，归纳证明的陈述是以 <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> 开始的。

<div class="paragraph"> </div>

    如果我们对目标中其他量词<b>后</b>的量化变量使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span>，那么它会自动
    引入全部被量词绑定的变量到上下文中。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">plus_comm''</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> + <span class="id" type="var">m</span> = <span class="id" type="var">m</span> + <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;这次让我们对&nbsp;<span class="inlinecode"><span class="id" type="var">m</span></span>&nbsp;而非&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span>&nbsp;进行归纳……&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">m</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">m'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">plus_n_O</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">IHm'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">plus_n_Sm</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab294"></a><h4 class="section">练习：1 星, standard, optional (plus_explicit_prop)</h4>
 以类似 <span class="inlinecode"><span class="id" type="var">mult_0_r''</span></span> 的方式来重写 <span class="inlinecode"><span class="id" type="var">plus_assoc'</span></span>，<span class="inlinecode"><span class="id" type="var">plus_comm'</span></span> 和它们的证明——
    对于每个定理，给出一个明确的命题的 <span class="inlinecode"><span class="id" type="keyword">Definition</span></span>，陈述定理并用归纳法证明这个
    定义的命题。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab295"></a><h1 class="section"><span class="inlinecode"><span class="id" type="keyword">Prop</span></span> 中的归纳法则</h1>

<div class="paragraph"> </div>

 之前，我们仔细学习了 Coq 为归纳定义的<b>集合</b>生成的归纳法则。 像 <span class="inlinecode"><span class="id" type="var">even</span></span>
    这样的归纳定义<b>命题</b>的归纳法则会复杂一点点。就全部归纳法则来说，我们想要
    通过使用 <span class="inlinecode"><span class="id" type="var">even</span></span> 的归纳法则并归纳地考虑 <span class="inlinecode"><span class="id" type="var">even</span></span> 中所有可能的形式来证明一些东西。
    然而，直观地讲，我们想要证明的东西并不是关于<b>证据</b>的陈述，而是关于
    <b>自然数</b>的陈述：因此，我们想要让归纳法则允许通过对证据进行归纳来
    证明关于数字的性质。

<div class="paragraph"> </div>

    比如，根据我们前面所讲，你可能会期待这样归纳定义的 <span class="inlinecode"><span class="id" type="var">even</span></span>……

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Inductive</span>&nbsp;<span class="id" type="var">even</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ev_0</span>&nbsp;:&nbsp;<span class="id" type="var">even</span>&nbsp;0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ev_SS</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>,&nbsp;<span class="id" type="var">even</span>&nbsp;<span class="id" type="var">n</span>&nbsp;→&nbsp;<span class="id" type="var">even</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;<span class="id" type="var">n</span>)).
<div class="paragraph"> </div>

</div>
    ……并给我们下面这样的归纳法则……

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ev_ind_max</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span>&nbsp;:&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>,&nbsp;<span class="id" type="var">even</span>&nbsp;<span class="id" type="var">n</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">O</span>&nbsp;<span class="id" type="var">ev_0</span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">m</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>)&nbsp;(<span class="id" type="var">E</span>&nbsp;:&nbsp;<span class="id" type="var">even</span>&nbsp;<span class="id" type="var">m</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">m</span>&nbsp;<span class="id" type="var">E</span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">P</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;<span class="id" type="var">m</span>))&nbsp;(<span class="id" type="var">ev_SS</span>&nbsp;<span class="id" type="var">m</span>&nbsp;<span class="id" type="var">E</span>))&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>)&nbsp;(<span class="id" type="var">E</span>&nbsp;:&nbsp;<span class="id" type="var">even</span>&nbsp;<span class="id" type="var">n</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">n</span>&nbsp;<span class="id" type="var">E</span>
<div class="paragraph"> </div>

</div>
     ……因为：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 由于 <span class="inlinecode"><span class="id" type="var">even</span></span> 被自然数 <span class="inlinecode"><span class="id" type="var">n</span></span> 所索引（任何 <span class="inlinecode"><span class="id" type="var">even</span></span> 对象 <span class="inlinecode"><span class="id" type="var">E</span></span> 都是某个自然数 <span class="inlinecode"><span class="id" type="var">n</span></span>
       是偶数的证据），且命题 <span class="inlinecode"><span class="id" type="var">P</span></span> 同时被 <span class="inlinecode"><span class="id" type="var">n</span></span> 和 <span class="inlinecode"><span class="id" type="var">E</span></span> 所参数化——因此，被用于证明断言的
       归纳法则同时涉及到一个偶数和这个数是偶数的证据。

<div class="paragraph"> </div>


</li>
<li> 由于有两种方法来给出偶数性质的证据（因为 <span class="inlinecode"><span class="id" type="var">even</span></span> 有两个构造子），我们应用归纳法则生成
       了两个子目标：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 须证明 <span class="inlinecode"><span class="id" type="var">P</span></span> 对 <span class="inlinecode">0</span> 和 <span class="inlinecode"><span class="id" type="var">ev_0</span></span> 成立。

<div class="paragraph"> </div>


</li>
<li> 须证明，当 <span class="inlinecode"><span class="id" type="var">n</span></span> 是一个自然数且 <span class="inlinecode"><span class="id" type="var">E</span></span> 是其偶数性质的证据，如果 <span class="inlinecode"><span class="id" type="var">P</span></span>
           对 <span class="inlinecode"><span class="id" type="var">n</span></span> 和 <span class="inlinecode"><span class="id" type="var">E</span></span> 成立，那么它也对 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> 和 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode"><span class="id" type="var">E</span></span> 成立。

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> 如果这些子目标可以被证明，那么归纳法则告诉我们 <span class="inlinecode"><span class="id" type="var">P</span></span> 对所有的偶数 <span class="inlinecode"><span class="id" type="var">n</span></span>
       和它们的偶数性质 <span class="inlinecode"><span class="id" type="var">E</span></span> 成立。

</li>
</ul>

<div class="paragraph"> </div>

    这比我们通常需要的或想要的更灵活一点：它为我们提供了一种方式证明逻辑断言，
    其断言涉及到一些关于偶数的证据的性质，然而我们真正想要的是证明某些<b>自然数</b>
    是偶数这样的性质——我们感兴趣的是关于自然数的断言，而非关于证据。如果对于命题 <span class="inlinecode"><span class="id" type="var">P</span></span>
    的归纳法则仅仅被 <span class="inlinecode"><span class="id" type="var">n</span></span> 所参数化，且其结论是 <span class="inlinecode"><span class="id" type="var">P</span></span> 对所有偶数 <span class="inlinecode"><span class="id" type="var">n</span></span> 成立，那会方便许多：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;... →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">even</span>&nbsp;<span class="id" type="var">n</span>&nbsp;→&nbsp;<span class="id" type="var">P</span>&nbsp;<span class="id" type="var">n</span>
<div class="paragraph"> </div>

</div>
    出于这样的原因，Coq 实际上为 <span class="inlinecode"><span class="id" type="var">even</span></span> 生成了简化过的归纳法则： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">even_ind</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;ev_ind<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:&nbsp;forall&nbsp;P&nbsp;:&nbsp;nat&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;Prop,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P&nbsp;0&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(forall&nbsp;n&nbsp;:&nbsp;nat,&nbsp;even&nbsp;n&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;P&nbsp;n&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;P&nbsp;(S&nbsp;(S&nbsp;n)))&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall&nbsp;n&nbsp;:&nbsp;nat,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;even&nbsp;n&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;P&nbsp;n&nbsp;*)</span><br/>
</div>

<div class="doc">
请特别注意，Coq 丢弃了命题 <span class="inlinecode"><span class="id" type="var">P</span></span> 参数中的证据项 <span class="inlinecode"><span class="id" type="var">E</span></span>。 
<div class="paragraph"> </div>

 若用自然语言来表述 <span class="inlinecode"><span class="id" type="var">ev_ind</span></span>，则是说：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 假设，<span class="inlinecode"><span class="id" type="var">P</span></span> 是关于自然数的一个性质（也即，<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 是一个在全体 <span class="inlinecode"><span class="id" type="var">n</span></span> 上的 <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>）。
      为了证明当 <span class="inlinecode"><span class="id" type="var">n</span></span> 是偶数时 <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 成立，需要证明：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">P</span></span> 对 <span class="inlinecode">0</span> 成立，

<div class="paragraph"> </div>


</li>
<li> 对任意 <span class="inlinecode"><span class="id" type="var">n</span></span>，如果 <span class="inlinecode"><span class="id" type="var">n</span></span> 是偶数且 <span class="inlinecode"><span class="id" type="var">P</span></span> 对 <span class="inlinecode"><span class="id" type="var">n</span></span> 成立，那么 <span class="inlinecode"><span class="id" type="var">P</span></span> 对 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> 成立。 
</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>

 正如期待的那样，我们可以不使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 而直接应用 <span class="inlinecode"><span class="id" type="var">ev_ind</span></span>。
    比如，我们可以使用它来证明 <span class="inlinecode"><span class="id" type="var">even'</span></span>（那个在 <a href="IndProp.html"><span class="inlineref">IndProp</span></a> 一章的练习中有点笨拙的偶数性质的定义）
    等价于更简洁的归纳定义 <span class="inlinecode"><span class="id" type="var">even</span></span>： 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_ev'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span class="id" type="var">even'</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">even_ind</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;ev_0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">even'_0</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;ev_SS&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">m</span> <span class="id" type="var">Hm</span> <span class="id" type="var">IH</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">even'_sum</span> 2 <span class="id" type="var">m</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">even'_2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">IH</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 定义的具体形式会影响到 Coq 生成的归纳法则。

<div class="paragraph"> </div>

    比如在 <a href="IndProp.html"><span class="inlineref">IndProp</span></a> 一章中，我们这样定义 <span class="inlinecode">≤</span>： 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Inductive&nbsp;le&nbsp;:&nbsp;nat&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;nat&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;Prop&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;le_n&nbsp;:&nbsp;forall&nbsp;n,&nbsp;le&nbsp;n&nbsp;n<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;le_S&nbsp;:&nbsp;forall&nbsp;n&nbsp;m,&nbsp;(le&nbsp;n&nbsp;m)&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;(le&nbsp;n&nbsp;(S&nbsp;m)).&nbsp;*)</span><br/>
</div>

<div class="doc">
这个定义其实可以被稍微简化一点，通过观察到左侧的参数 <span class="inlinecode"><span class="id" type="var">n</span></span>
    在定义中始终是相同的，我们可把它变成整体定义中的一个“一般参数”，而非每个构造子的参数。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">le</span> (<span class="id" type="var">n</span>:<span class="id" type="var">nat</span>) : <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">le_n</span> : <span class="id" type="var">le</span> <span class="id" type="var">n</span> <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">le_S</span> <span class="id" type="var">m</span> (<span class="id" type="var">H</span> : <span class="id" type="var">le</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>) : <span class="id" type="var">le</span> <span class="id" type="var">n</span> (<span class="id" type="var">S</span> <span class="id" type="var">m</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "m ≤ n" := (<span class="id" type="var">le</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span>).<br/>
</div>

<div class="doc">
尽管第二个看起来不那么对称了，但它却更好一点。为什么呢？因为它会生成更简单的归纳法则。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">le_ind</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;&nbsp;forall&nbsp;(n&nbsp;:&nbsp;nat)&nbsp;(P&nbsp;:&nbsp;nat&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;Prop),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;P&nbsp;n&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(forall&nbsp;m&nbsp;:&nbsp;nat,&nbsp;n&nbsp;&lt;=&nbsp;m&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;P&nbsp;m&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;P&nbsp;(S&nbsp;m))&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall&nbsp;n<sub>0</sub>&nbsp;:&nbsp;nat,&nbsp;n&nbsp;&lt;=&nbsp;n<sub>0</sub>&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;P&nbsp;n<sub>0</sub>&nbsp;*)</span><br/>
</div>

<div class="doc">
<a name="lab296"></a><h1 class="section">形式化 vs. 非形式化的归纳证明</h1>

<div class="paragraph"> </div>

 问：命题 <span class="inlinecode"><span class="id" type="var">P</span></span> 的形式化证明和同一个命题 <span class="inlinecode"><span class="id" type="var">P</span></span> 的非形式化证明之间是什么关系？

<div class="paragraph"> </div>

    答：后者应当<b>教给</b>读者如何产生前者。

<div class="paragraph"> </div>

    问：需要多少的细节？

<div class="paragraph"> </div>

    不幸的是，并没有一个正确的答案；当然了，其实有一系列的选择。

<div class="paragraph"> </div>

    一种选择是，我们可以为读者给出全部的形式化证明（也即，“非形式化的”证明只是把
    形式化的证明用文字表述出来）。这可能让读者有能力自己完成形式化的证明，但也许
    并没有<b>教给</b>读者什么东西。

<div class="paragraph"> </div>

  而另一种选择则是，我们可以说“某个定理为真，如果你觉得它有些困难那么可以自己尝试把它搞明白。”
  这也不是一种很好的教学策略，因为书写证明常常需要一两个对于要证明的东西的重要洞察，
  而多数读者往往在自己发现这些这些洞察前已经放弃了。

<div class="paragraph"> </div>

  一种中庸之道是——我们提供含有重要洞察的证明（免去读者像我们一开始一样辛苦地寻找证明），
  加上模式化部分的高层次建议（比如，归纳假设是什么，以及归纳证明中每个情形的证明责任），
  这样帮助读者节省自己重新构造这些东西的时间，但不会有过多的细节以至于主要的概念和想法受到干扰。

<div class="paragraph"> </div>

  我们在本章中已经仔细查看了形式化的归纳证明的“底层原理”，现在是时候来看看非形式化的归纳证明了。

<div class="paragraph"> </div>

  在现实世界的数学交流中，证明的书写既有冗长的，也有非常简洁的。
  尽管理想状态是二者中间的某种形式，但从有一点冗长的证明开始学习是有好处的。
  同时，在学习的过程中，有一个明确的标准来进行比较也是有益的。为此，
  我们提供了两份模板：一份用于归纳证明<b>数据</b>（也即，<span class="inlinecode"><span class="id" type="keyword">Type</span></span> 中我们进行归纳的东西），
  另一份用于归纳证明<b>证据</b>（也即，<span class="inlinecode"><span class="id" type="keyword">Prop</span></span> 中归纳定义的东西）。
<div class="paragraph"> </div>

<a name="lab297"></a><h2 class="section">对归纳定义的集合进行归纳</h2>

<div class="paragraph"> </div>

 <b>模板</b>：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <b>定理</b>： &lt;有形如“For all <span class="inlinecode"><span class="id" type="var">n</span>:<span class="id" type="var">S</span></span>, <span class="inlinecode"><span class="id" type="var">P</span>(<span class="id" type="var">n</span>)</span>”的全称量化命题，其中 <span class="inlinecode"><span class="id" type="var">S</span></span>
          是某个归纳定义的集合。&gt;

<div class="paragraph"> </div>

         <b>证明</b>： 对 <span class="inlinecode"><span class="id" type="var">n</span></span> 进行归纳。

<div class="paragraph"> </div>

           &lt;<span class="inlinecode"><span class="id" type="var">S</span></span> 中的每个构造子 <span class="inlinecode"><span class="id" type="var">c</span></span> 的情形……&gt;

<div class="paragraph"> </div>

<ul class="doclist">
<li> 假设 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" type="var">ak</span></span>，其中 &lt;…… 这里我们为每个具有类型 <span class="inlinecode"><span class="id" type="var">S</span></span> 的 <span class="inlinecode"><span class="id" type="var">a</span></span> 陈述其归纳假设（IH）&gt; 。
             我们需要证明 &lt;…… 我们在这里重新陈述 <span class="inlinecode"><span class="id" type="var">P</span>(<span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" type="var">ak</span>)</span>&gt;。

<div class="paragraph"> </div>

             &lt;继续并证明 <span class="inlinecode"><span class="id" type="var">P</span>(<span class="id" type="var">n</span>)</span> 来完成这个情形……&gt;

<div class="paragraph"> </div>


</li>
<li> &lt;其他情形以此类推……&gt;                        <span class="proofbox">&#9744;</span>

</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>

    <b>举例</b>:

<div class="paragraph"> </div>

<ul class="doclist">
<li> <b>定理</b>: 对所有集合 <span class="inlinecode"><span class="id" type="var">X</span></span>， 列表 <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>，以及数字 <span class="inlinecode"><span class="id" type="var">n</span></span>，如果
          <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> 那么 <span class="inlinecode"><span class="id" type="var">index</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">None</span></span>。

<div class="paragraph"> </div>

        <b>证明</b>: 对 <span class="inlinecode"><span class="id" type="var">l</span></span> 进行归纳。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 假设 <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode">[]</span>。我们需要证明，对于任意数字 <span class="inlinecode"><span class="id" type="var">n</span></span>，如果 <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode">[]</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span>，那么
         <span class="inlinecode"><span class="id" type="var">index</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> <span class="inlinecode">[]</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">None</span></span>。

<div class="paragraph"> </div>

          可从 <span class="inlinecode"><span class="id" type="var">index</span></span> 的定义中直接得出。

<div class="paragraph"> </div>


</li>
<li> 假设 <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">::</span> <span class="inlinecode"><span class="id" type="var">l'</span></span> 对某个 <span class="inlinecode"><span class="id" type="var">x</span></span> 和 <span class="inlinecode"><span class="id" type="var">l'</span></span>，其中 <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">l'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n'</span></span> 对任意数字 <span class="inlinecode"><span class="id" type="var">n'</span></span>
          蕴含了 <span class="inlinecode"><span class="id" type="var">index</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span> <span class="inlinecode"><span class="id" type="var">l'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">None</span></span>。我们需要证明，对任意数字 <span class="inlinecode"><span class="id" type="var">n</span></span>，如果
          <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode">(<span class="id" type="var">x</span>::<span class="id" type="var">l'</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> 那么 <span class="inlinecode"><span class="id" type="var">index</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> <span class="inlinecode">(<span class="id" type="var">x</span>::<span class="id" type="var">l'</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">None</span></span>。

<div class="paragraph"> </div>

          设 <span class="inlinecode"><span class="id" type="var">n</span></span> 为数字且 <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span>。因为

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">length</span>&nbsp;<span class="id" type="var">l</span>&nbsp;=&nbsp;<span class="id" type="var">length</span>&nbsp;(<span class="id" type="var">x</span>::<span class="id" type="var">l'</span>)&nbsp;=&nbsp;<span class="id" type="var">S</span>&nbsp;(<span class="id" type="var">length</span>&nbsp;<span class="id" type="var">l'</span>),
<div class="paragraph"> </div>

</div>
          需要证明

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">index</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;(<span class="id" type="var">length</span>&nbsp;<span class="id" type="var">l'</span>))&nbsp;<span class="id" type="var">l'</span>&nbsp;=&nbsp;<span class="id" type="var">None</span>.
<div class="paragraph"> </div>

</div>
          若选取 <span class="inlinecode"><span class="id" type="var">n'</span></span> 为 <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">l'</span></span> 这可从归纳假设中直接得出。  <span class="proofbox">&#9744;</span> 
</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>

<a name="lab298"></a><h2 class="section">对归纳定义的命题进行归纳</h2>

<div class="paragraph"> </div>

 由于归纳定义的证明对象经常被称作“导出树（derivation trees）”，这种形式的
    证明也被叫做<b>在导出式上归纳</b>。
    <b>模板</b>：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <b>定理</b>: &lt;有形如“<span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span>”的命题，其中 <span class="inlinecode"><span class="id" type="var">Q</span></span> 是某个归纳定义的命题
        （更一般地，“对任意 <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> <span class="inlinecode"><span class="id" type="var">z</span></span>，<span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> <span class="inlinecode"><span class="id" type="var">z</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> <span class="inlinecode"><span class="id" type="var">z</span></span>”）&gt;

<div class="paragraph"> </div>

         <b>证明</b>: 对 <span class="inlinecode"><span class="id" type="var">Q</span></span> 的导出式进行归纳。&lt;或者，更一般地，“假设给定 <span class="inlinecode"><span class="id" type="var">x</span></span>，<span class="inlinecode"><span class="id" type="var">y</span></span> 和
         <span class="inlinecode"><span class="id" type="var">z</span></span>。通过对 <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> <span class="inlinecode"><span class="id" type="var">z</span></span> 的导出式进行归纳，我们证明 <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> <span class="inlinecode"><span class="id" type="var">z</span></span> 蕴含 <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span> <span class="inlinecode"><span class="id" type="var">z</span></span>”……&gt;

<div class="paragraph"> </div>

           &lt;<span class="inlinecode"><span class="id" type="var">Q</span></span> 中的每个构造子 <span class="inlinecode"><span class="id" type="var">c</span></span> 的情形……&gt;

<div class="paragraph"> </div>

<ul class="doclist">
<li> 假设被用于证明 <span class="inlinecode"><span class="id" type="var">Q</span></span> 的最终规则是 <span class="inlinecode"><span class="id" type="var">c</span></span>。那么&lt;……我们在这里陈述所有 <span class="inlinecode"><span class="id" type="var">a</span></span> 的类型，
            从构造子的定义中得到的任何等式，以及每个具有类型 <span class="inlinecode"><span class="id" type="var">Q</span></span> 的 <span class="inlinecode"><span class="id" type="var">a</span></span> 的归纳假设&gt;。
            我们需要证明&lt;……我们在这里重新陈述 <span class="inlinecode"><span class="id" type="var">P</span></span>&gt;。

<div class="paragraph"> </div>

             &lt;继续并证明 <span class="inlinecode"><span class="id" type="var">P</span></span> 来完成这个情形……&gt;

<div class="paragraph"> </div>


</li>
<li> &lt;其他情形以此类推……&gt;                        <span class="proofbox">&#9744;</span>

</li>
</ul>

</li>
</ul>

<div class="paragraph"> </div>

    <b>举例</b>

<div class="paragraph"> </div>

<ul class="doclist">
<li> <b>定理</b>: <span class="inlinecode">≤</span> 关系是传递的，也即，对任意数字 <span class="inlinecode"><span class="id" type="var">n</span></span>，<span class="inlinecode"><span class="id" type="var">m</span></span> 和 <span class="inlinecode"><span class="id" type="var">o</span></span>，如果
         <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">m</span></span> 且 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">o</span></span> 那么 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">o</span></span>。

<div class="paragraph"> </div>

         <b>证明</b>: 对 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">o</span></span> 的导出式进行归纳。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 假设被用于证明 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">o</span></span> 的最终规则是 <span class="inlinecode"><span class="id" type="var">le_n</span></span>。
             那么 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">o</span></span> 且我们需要证明 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">m</span></span>，其可从假设中直接得出。

<div class="paragraph"> </div>


</li>
<li> 假设被用于证明 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">o</span></span> 的最终规则是 <span class="inlinecode"><span class="id" type="var">le_S</span></span>。
             那么 <span class="inlinecode"><span class="id" type="var">o</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">o'</span></span> 对某个 <span class="inlinecode"><span class="id" type="var">o'</span></span> 且 <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">o'</span></span>。我们需要证明 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">o'</span></span>。
             由归纳假设得出，<span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">o'</span></span>。

<div class="paragraph"> </div>

            因此，根据 <span class="inlinecode"><span class="id" type="var">le_S</span></span>，<span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">o'</span></span>。  <span class="proofbox">&#9744;</span> 
</li>
</ul>

</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>